package org.gap.jseed.contract.example;

import java.util.LinkedList;

import org.gap.jseed.contract.annotation.Condition;
import org.gap.jseed.contract.annotation.Ensure;
import org.gap.jseed.contract.annotation.Invariant;
import org.gap.jseed.contract.annotation.NotNull;
import org.gap.jseed.contract.annotation.Require;

@Invariant(@Condition(
		label="size() never negative", 
		value="size() >= 0"))
public class ContractedStack {
	private int size = 0;
	private LinkedList<Object> container = new LinkedList<Object>();
	
	public boolean isEmpty() {
		return size() == 0;
	}

	public int size() {
		return size;
	}

	@NotNull
	@Ensure({
		@Condition(
			label="size increases", 
			value="old:int size() + 1 == size()"),
		@Condition(
			label="object in peek()", 
			value="peek() == $1")})
	public void push(Object object) {
		container.add(0, object);
		size++;
	}

	public Object peek() {
		return container.get(0);
	}

	@Require(
			@Condition(
				label="Not empty",
				value="!isEmpty()"))
	@Ensure(
			@Condition(
				label="Size decreased",
				value="old:int size() - 1 == size()"))
	public void pop() {
		size--;
		container.remove(size);
	}

	@Require({
		@Condition(
				label="index big enough",
				value="$1 >= 0"),
		@Condition(
				label="index small enough",
				value="$1 < size()")}) 
	public Object itemAt(int index) {
		return container.get(index);
	}

}
